import os
import sys
import yaml
import json
import subprocess
from datetime import datetime
from jinja2 import Environment, FileSystemLoader
import argparse
from typing import Dict, Any
import jinja2
from pathlib import Path

class FormalToolkit:
    """形式验证全流程管理工具"""
    
    def __init__(self, cover_mode):
        # 获取formal目录的绝对路径
        formal_dir = Path(__file__).resolve().parent.parent
        # 更改测试模式
        # 读取模板文件
        with open(formal_dir / "configs/default.yaml", 'r', encoding='utf-8') as f:
            yaml_content = f.read()
        # 确定 cover_mode 值（确保为字符串）
        cover_mode_val = '1' if cover_mode else '0'
        # 替换占位符
        config = yaml_content.replace('{{cover_mode}}', cover_mode_val)

        # 写入新配置文件
        with open(formal_dir /"configs/config.yaml", 'w', encoding='utf-8') as f:
            f.write(config)
        
        # 处理配置文件路径
        config_path = str(formal_dir / "configs/config.yaml")
        self.config = self._load_config(config_path)
        

        # 确保模板路径是绝对路径
        templates_dir = str(formal_dir / "templates")
        self.env = jinja2.Environment(loader=jinja2.FileSystemLoader(templates_dir))
        # 调用方法时不传递参数
        self.results_dir = self._create_results_dir()

    def _load_config(self, path: str) -> Dict[str, Any]:
        """加载 YAML 配置文件"""
        with open(path, "r") as f:
            return yaml.safe_load(f)
    
    def _create_results_dir(self) -> str:
        """创建带时间戳的结果目录（使用绝对路径）"""
        formal_dir = Path(__file__).resolve().parent.parent
        base_results_dir = str(formal_dir / "results")
        # 确保基础目录存在
        os.makedirs(base_results_dir, exist_ok=True)
        # 创建带时间戳的子目录
        timestamp = datetime.now().strftime("%Y%m%d_%H%M%S")
        results_dir = os.path.join(base_results_dir, f"run_{timestamp}")
        os.makedirs(results_dir, exist_ok=True)
        return results_dir
    
    def generate_sby_config(self) -> str:
        """使用 Jinja2 生成 SBY 配置文件"""
        template = self.env.get_template(self.config["sby_template"])
        sby_content = template.render(**self.config["sby_params"])
        
        sby_path = os.path.join(self.results_dir, "config.sby")
        with open(sby_path, "w") as f:
            f.write(sby_content)

        print(f"[DEBUG] SBY 配置文件已生成: {os.path.abspath(sby_path)}")
        return sby_path
    
    def run_formal(self, sby_path: str) -> Dict[str, Any]:
        """运行 SymbiYosys 并捕获结果"""
        cmd = ["sby", "-f", sby_path, "-d", self.results_dir]
        process = subprocess.Popen(
            cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True
        )
        
        # 实时输出日志到控制台和文件
        log_path = os.path.join(self.results_dir, "sby.log")
        with open(log_path, "w") as log_file:
            for line in process.stdout:
                sys.stdout.write(line)
                log_file.write(line)
        
        process.wait()
        return self._parse_sby_results()
    
    def _parse_sby_results(self) -> Dict[str, Any]:
        """解析 SBY 结果文件"""
        status_path = os.path.join(self.results_dir, "status")
        with open(status_path, "r") as f:
            status_content = f.read()
        
        result = {
            "pass": "PASS" in status_content,
            "log": status_content,
            "traces": [],
            "coverage": self._parse_coverage(),
        }
        
        # 收集反例波形路径
        for engine_dir in os.listdir(self.results_dir):
            if engine_dir.startswith("engine_"):
                trace_path = os.path.join(self.results_dir, engine_dir, "trace.vcd")
                if os.path.exists(trace_path):
                    result["traces"].append(trace_path)
        
        return result
    
    def _parse_coverage(self) -> Dict[str, float]:
        """解析覆盖率结果（需根据工具输出定制）"""
        # 示例：从日志中提取覆盖率数据
        return {"toggle": 95.0, "fsm": 80.0}  # 伪代码
    
    def generate_report(self, result: Dict[str, Any]) -> str:
        """生成 HTML 报告"""
        template = self.env.get_template("report_template.html.j2")
        html_content = template.render(
            config=self.config,
            result=result,
            timestamp=datetime.now().strftime("%Y-%m-%d %H:%M:%S")
        )
        
        report_path = os.path.join(self.results_dir, "report.html")
        with open(report_path, "w") as f:
            f.write(html_content)
        
        return report_path
    
    def open_waveform(self, trace_path: str):
        """调用波形查看器（如 gtkwave）"""
        if sys.platform == "linux":
            subprocess.Popen(["gtkwave", trace_path])
        elif sys.platform == "win32":
            subprocess.Popen(["C:\\Program Files\\gtkwave\\bin\\gtkwave.exe", trace_path])
    
    def interactive_debug(self, result: Dict[str, Any]):
        """交互式调试菜单"""
        if not result["pass"] and result["traces"]:
            choice = input("\n验证失败，选择操作 [V]iew waveform/[R]etry/[I]gnore: ").lower()
            if choice == "v":
                self.open_waveform(result["traces"][0])
            elif choice == "r":
                self.run_formal(self.generate_sby_config())

def main():
    parser = argparse.ArgumentParser(description="形式验证自动化工具")
    parser.add_argument("--config", default="../configs/default.yaml", help="配置文件路径")
    parser.add_argument("--report", action="store_true", help="生成HTML报告")
    parser.add_argument("--mode", nargs='+', help="指定验证模式（覆盖配置文件）")
    parser.add_argument("--engines", nargs='+', help="指定验证引擎列表（覆盖配置文件）")
    args = parser.parse_args()
    
    toolkit = FormalToolkit()
    sby_path = toolkit.generate_sby_config()
    result = toolkit.run_formal(sby_path)
    
    if args.report:
        report_path = toolkit.generate_report(result)
        print(f"报告已生成: file://{os.path.abspath(report_path)}")
    
    if not result["pass"]:
        toolkit.interactive_debug(result)

if __name__ == "__main__":
    main()